/**
 * Copyright (c) 2010-2011 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.prover;

import java.io.IOException;

import com.googlecode.syper.javasyp.config.JavaSypPreferences;

/**
 * Factory for {@link SmtSolverZ3} objects that uses a process factory
 * to create Z3 processes based on Eclipse preferences set when the
 * factory is created
 * Allocate a new factory whenever you want preference changes to take effect.
 * @author kevin
 * @since Oct 24, 2010
 */
class Z3Factory {

	private final ProcessBuilder z3builder;

	public Z3Factory() {
		// Z3 seems to use / on Windows but - on Ubuntu for command-line options
		char opt = isWindows() ? '/' : '-';
		if (requestModels()) {
			z3builder = new ProcessBuilder(getExecutablePath(),
					opt + "smt", // SMT-LIB input format
					opt + "T:" + getTimeoutSeconds(), // timeout
					opt + "in",  // read from stdin
					opt + "m");  // print model if satisfiable
		} else {
			z3builder = new ProcessBuilder(getExecutablePath(),
					opt + "smt", // SMT-LIB input format
					opt + "T:" + getTimeoutSeconds(), // timeout
					opt + "in");  // read from stdin
		}
		// merge stderr with stdout
		z3builder.redirectErrorStream(true);
	}

	public SmtSolverZ3 create() throws IOException {
		// TODO allow turning off input/output
		return new SmtSolverZ3(z3builder.start(), true);
	}

	public int getTimeoutSeconds() {
		return JavaSypPreferences.getInstance().getTimeoutSeconds(
				JavaSypPreferences.SMT_SOLVER_Z3);
	}

	private static String getExecutablePath() {
		return JavaSypPreferences.getInstance().getExecutable(
				JavaSypPreferences.SMT_SOLVER_Z3);
	}

	private static boolean requestModels() {
		return JavaSypPreferences.getInstance().isCounterexamplesRequested();
	}

	private static boolean isWindows() {
		String os = System.getProperty("os.name");
		return os.contains("Win");
	}
}
